| |
VOLUME 5, ISSUE 4, PAPER 2
|
A Step-indexed Semantics of Imperative Objects
|
©Catalin Hritcu, Saarland University
©Jan Schwinghammer, Saarland University
|
Abstract
Step-indexed semantic interpretations of types were proposed as an
alternative to purely syntactic proofs of type safety using subject reduction.
The types are interpreted as sets of values indexed by the number of
computation steps for which these values are guaranteed to behave like proper
elements of the type. Building on work by Ahmed, Appel and others, we introduce
a step-indexed semantics for the imperative object calculus of Abadi and
Cardelli. Providing a semantic account of this calculus using more
`traditional', domain-theoretic approaches has proved challenging due to the
combination of dynamically allocated objects, higher-order store, and an
expressive type system. Here we show that, using step-indexing, one can
interpret a rich type discipline with object types, subtyping, recursive and
bounded quantified types in the presence of state.
|
Publication date: December 18, 2009
Full Text: PDF | PostScript
DOI: 10.2168/LMCS-5(4:2)2009
Hit Counts: 1023 |
 Creative Commons | |
